Lean is an open-source functional programming language that makes it easy to write correct and maintainable code

WHY LEAN?

PRIMARY USE CASES

“Lean has become a key enabler in scaling automated reasoning at Amazon. Its capacity to verify complex systems involving advanced mathematical concepts has transformed how we tackle problems once thought too complex or impractical. Lean is an indispensable tool in modern, large-scale software engineering, helping ensure soundness, correctness and verified AI across our systems.” — Byron Cook, Vice President and Distinguished Scientist, AWS

IN THE NEWS

Is Math the Path to Chatbots that Don’t Make Stuff Up? (NY Times)

“Chatbots can answer questions, write poetry, summarize news articles and generate images. But they also make mistakes that defy common sense. And sometimes, they make stuff up — a phenomenon called hallucination. But researchers are building new A.I. systems [with Lean] that can verify their own math — and maybe more.”

AI Will Become Mathematicians’ ‘Co-Pilot’ (Scientific American)

In this Scientific American interview, Terence Tao talks about how automated proof checkers like Lean are revolutionizing how mathematicians collaborate on increasingly complex problems.

“AlphaProof uses the Gemini large language model to convert naturally phrased math questions into a programming language called Lean. This provides the training fodder for a second algorithm to learn, through trial and error, how to find proofs that can be confirmed as correct.”

Google DeepMind’s Game-Playing AI Tackles a Chatbot Blind Spot (Wired)

FEATURED PROJECTS

AMAZON SCIENCE LEAN USE CASES

AWS is using Lean to solve complex software verification and modeling challenges.

THE FERMAT’S LAST THEOREM PROJECT

Kevin Buzzard’s ambitious project to “crowd-source mathematics” and prove Fermat’s Last Theorem in Lean.

MATHEMATICAL SUPERINTELLIGENCE (MSI)

Harmonic’s MSI Platform, which uses Lean to eliminate AI hallucinations.

  • "Lean enables large-scale collaboration by allowing mathematicians to break down complex proofs into smaller, verifiable components. This formalization process ensures the correctness of proofs and facilitates contributions from a broader community. With Lean, we are beginning to see how AI can accelerate the formalization of mathematics, opening up new possibilities for research." —Terence Tao, Fields Medalist and Professor of Mathematics, UCLA

  • “At Google DeepMind, we used Lean to build AlphaProof, a new reinforcement-learning based system for formal math reasoning. Lean’s extensibility and verification capabilities were key in enabling the development of AlphaProof.” — Pushmeet Kohli, Vice President, Research Google DeepMind

  • "MSI [with Lean] will play a critical role in any industry where safety is paramount, including aerospace, automotive, and medical technology. In addition, we look forward to providing early access to our technology to students and researchers to accelerate advancement in mathematics, science, and engineering."—Tudor Achim, Co-Founder and CEO of Harmonic

THANK YOU TO OUR DONORS AND PARTNERS